R-interface(A;B)
== l:IdLnk, tg:Id. R-da(A;source(l))(rcv(l,tg))?Void  R-da(B;destination(l))(rcv(l,tg))?Top 

latex

---

clarification:

R-interface(A;B)
== l:IdLnk, tg:Id.
== fpf-cap(R-da(A;source(l));KindDeq;rcv(l,tg);Void)
==  fpf-cap(R-da(B;destination(l));KindDeq;rcv(l,tg);Top) 

latex

Definitions	IdLnk, x:A. B(x), Id, source(l), Void, f(x)?z, R-da(R;i), destination(l), KindDeq, rcv(l,tg), Top
FDL editor aliases	R-interface